(* 
 *  PDP ML
 *  
 *    Francesco Cotto
 *
 *    Es. sui costruttori di tipo: Numeri di Peano
 *)

type nat = Zero | Succ of nat ;;


(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
(* * * * * * * * * * * *Operatori di confronto * * * * * * * * * * * * * * * *)
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)

	
let rec ( =+ ) m n = match (m,n) with
	 (Zero,   Zero  ) -> true
	|(Succ _, Zero  ) -> false
	|(Zero  , Succ _) -> false
	|(Succ t, Succ z) -> t =+ z ;;

let rec ( >+ ) m n = match (m,n) with
	 (Zero,   Zero  ) -> false
	|(Succ _, Zero  ) -> true
	|(Zero  , Succ _) -> false
	|(Succ t, Succ z) -> t >+ z ;;
	
let ( >=+ ) m n = (m >+ n) or (m =+ n)  ;;

let ( <+ ) m n = not ( m >=+ n) ;;

let ( <=+ ) m n = not ( m >+ n) ;;


(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
(* * * * * * * * * * * * *Operazioni aritmetiche * * * * * * * * * * * * * * *)
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)


(* x + S(y) = S(x + y) 
 * x + 0 = x
 *)
let rec ( ++ ) m n = match m with
	  Zero -> n
	| Succ k -> Succ(k ++ n);;


(*  x * S(y) = x + (x * y)   *)
let rec ( *+ ) m n = match m with
          Zero -> Zero
	 |Succ Zero -> n
	 |Succ k    -> n ++ (k *+ n) ;;


(* x - 0 = x  
 * S(x) - S(y) = x - y
 *)	 
let rec ( -+ ) m n = match (m,n) with
         (Zero, _) -> Zero 
	|(k, Zero) -> k
	|(Succ t, Succ v) -> t -+ v ;;

	
let rec ( /+ ) m n = 
   if (m >=+ n) then Succ Zero ++ ( (m -+ n) /+ n )
                                  else Zero ;;

                                 	
(* m mod n = m-n mod n  *)	
let rec modp m n = 
   if (m =+ Zero) then Zero
                 else if ( m >=+ n ) then modp (m -+ n) n
                                      else m ;;

(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
(* * * * * * * * * * * * * * * * Cast* * * * * * * * * * * * * * * * * * * * *)
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
                                      

let rec np_of_int n = if (n > 0) then Succ ( np_of_int (n-1) )
                              else Zero ;;
                              
let rec int_of_np n = if (n >+ Zero) then 1 + int_of_np (n -+ Succ Zero)
                                     else 0 ;;
                                     
let rec string_of_np n = 
   match n with
       Zero -> "Zero"
      |Succ Zero -> "Succ Zero" 
      |Succ k    -> "Succ ("^(string_of_np k)^")";;                                     

(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)
(* * * * * * * * * * * * * * * * Test* * * * * * * * * * * * * * * * * * * * *)
(* * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * * *)


print_string "3 = " ; np_of_int 3 ;;
print_string "(Succ Zero)" ; int_of_np (Succ Zero) ;;      

let testOp m op opStr n  = 
   print_string ( (string_of_int m)^" "^opStr^" "^(string_of_int n)^"=" );
   (op (np_of_int m) (np_of_int n) ) ;;

testOp 1 (=+) "=" 1 ;;
testOp 2 (=+) "=" 1 ;;
testOp 3 (>+) ">" 2 ;;
testOp 4 (<=+)"<="  3 ;;

testOp 1 (++) "+" 1 ;;
testOp 1 ( *+ ) "*" 1 ;;
testOp 1 (-+) "-" 1 ;;
testOp 1 (/+) "/" 1 ;;
testOp 1 modp "mod" 1 ;;
